The notation for this is in a way algebra of f.
So now in a category I have to say what the objects are, what the morphisms are and why this is a category.
The objects here, they remind a bit of algebra from the universal algebra or algebra from the algebra.
What are algebra? These are always quantities with some operations.
Here we have no quantities, here we have a basic category on which the filter runs.
So what else are the quantities? This is simply an object in the category A.
And then an algebra has a structure.
So in quantities there are operations that fulfill some equations, for example.
And here it is simply a morphism in the category from f from A to A.
Have you ever seen something like this? No.
Good, then it is also necessary to repeat this here.
So objects in this category as f, these are pairs where A is an object of C.
And this is a morphism of C.
So, and if I now have two such devices, what are the morphisms from one such thing to another?
So now I have one such algebra and another one B with its structure.
This is written formally after that it is now a commutative square, which is not the case.
So morphism from AA to AA to BBB is a morphism in C.
So that when I apply my function to the morphism, the whole thing becomes a commutative square.
So the morphism is h from A to B in C, so that this commutative square commutes.
Now you have to calculate that this really provides a category, that the identity is a morphism from A to itself.
You might see that directly when I make an identity morphism from A to A and here f from identity.
Then it is identity again, so then it is written as A equals A.
And if I have two such morphisms, one from A to B and then another one somewhere else, to C,
then I can compose in the basic category.
I am not going through the X here, so that is basically a joint of two commutative squares,
which then provides the homomorphism, as they are called, algebra morphism or homomorphism, that they compose.
So, that is formal, what f-algebras are, and now let's look at a few examples of why we would be interested in this,
especially if you come from computer science and we take the quantities as the basic category, because they are so easy.
But of course you can also take other basic categories, for example, semi-ordinated quantities,
so if you put pos, you get semi-ordinated algebra or CPUs or topological spaces or even more complicated things.
So, and a function of quantity, that is basically, you can also understand it as a kind of quantity construction,
that takes a quantity and delivers another quantity back, which is somehow different,
so something is assigned to it, something is constructed with it, in this case, an element of the junction is simply combined with it.
This is the simplest possible quantity construction that you can imagine, apart from identity.
And I often only write what the function of objects does in the assumption that they already understand what the homomorphism does.
Because if I now use a representation here, then I can also make 1 plus f.
Is it clear to you what that is, if you add an element to a representation, so the identity representation on the quantity,
but what this plus does, or should I go back to it again?
Maybe go back to it briefly.
So you can, yes, you actually need products and coproducts for this,
but well, on quantities we can say it quite easily, so if I have something from a to b and from c to d, f, g,
let's do the simple thing first, which you can imagine immediately, if you write a cartesian product in between.
Then you have a cross c, b cross d and f cross g.
And that of course does what you would expect, if I have an element there,
then this is of course depicted from this f cross g to f a, g c.
And that's in here, that's a bit of a miscalculation,
but that's how you would multiply functions together cartesian.
So what about the unification? So if I now take a plus c and here b plus d, what does f plus g do?
So the unification is called unification and I make sure that nothing is identified here,
so elements are still separated.
Presenters
Zugänglich über
Offener Zugang
Dauer
01:29:40 Min
Aufnahmedatum
2017-10-23
Hochgeladen am
2019-04-20 08:09:03
Sprache
de-DE
Die behandelten Themen bauen auf den Stoff von Algebra des Programmierens auf und vertieft diesen.
Folgende weiterführende Themen werden behandelt:
-
Kategorie der CPOs; insbesondere freie CPOs, Einbettungen/Projektionen, Limes-Kolimes-Koinzidenz
-
Lokal stetige Funktoren und deren kanonische Fixpunkte; Lösung rekursiver Bereichsgleichungen insbesondere Modell des ungetyptes Lambda-Kalküls
-
freie Konstruktionen, universelle Pfeile und adjungierte Funktoren
-
Äquivalenzfunktoren
-
Monaden: Eilenberg-Moore und Kleisli-Kategorien; Freie Monaden; Becks Satz
-
evtl. Distributivgesetze, verallgemeinerte Potenzmengenkonstruktion und abstrakte GSOS-Regeln
-
evtl. Algebren und Monaden für Iteration
Lernziele und Kompetenzen:
Fachkompetenz Verstehen Die Studierenden erklären grundlegende Begriffe und Konzepte der Kategorientheorie und beschreiben Beispiele. Sie erklären außerdem grundlegende kategorielle Ergebnisse. Anwenden Die Studierenden wenden kategorientheoretische Konzepte und Ergebnisse an, um semantische Modelle für Programmiersprachen und Spezifikationsformalismen aufzustellen. Analysieren Die Studierenden analysieren kategorientheoretische Beweise, dieskutieren die entsprechende Argumentationen und legen diese schriftlich klar nieder. Lern- bzw. Methodenkompetenz Die Studieren lesen und verstehen Fachliteratur, die die Sprache der Kategorientheorie benutzt.
Sie sind in der Lage entsprechende mathematische Argumentationen nachzuvollziehen, zu erklären und selbst zu führen und schriftlich darzus